Step of Proof: nat_ind_tp 9,38
Inference at * 1 1 1 3 1 2 
Iof proof for Lemma nat ind tp:



1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. i : 
5. 0 < i
6. P(i - 1)
  P(i) 
latex
 by AddHiddenLabel `upcase` 
latex

 1: .....upcase..... NILNIL

 1:   P(i)
 .

origin